#!/bin/bash

##################
# Return values:
# 1: parameters or files error
# 2: SAT Solver error
# 10: CPU and GPU solvers outputs match (passed)
# 20: CPU and GPU solvers outputs do not match (failed)
#
##################

# Temporary files
DATE=`date +"%y_%m_%d_%H_%M_%S"`
TMP_FILE=/tmp/test_cnf_${DATE}_${RANDOM}

# Input files
FILES_PREFIX=$1
CNF=${FILES_PREFIX}".cnf"
SOLUTIONS_FILE=${FILES_PREFIX}".solutions"

# Executables
CUDAPSAT=../Debug/GPUSATSolver

if [[ "$#" != 1 ]] && [[ "$#" != 2 ]] && [[ "$#!" != 3 ]]
then
	echo "Wrong number of parameters. Expected 1, 2 or 3." >&2
	exit 1
fi

if ! [[ -e "$CNF" ]]
then
	echo "Could not find the CNF file." >&2
	exit 1
fi

if ! [[ -e "$SOLUTIONS_FILE" ]]
then
	echo "Could not find the solutions file." >&2
	exit 1
fi

if [[ "$#" == 1 ]]
then
	THREADS=1
	FORCE_PARALLEL=""
else
	THREADS=$2

	if [[ "$THREADS" == "0" ]]
	then
		echo "Invalid threads number, should be a positive integer (if you recall your math classes, zero is not a positive integer)." >&2
		exit 1

	fi

	if ! [[ "$THREADS" =~ [1-9][0-9]* ]]
	then
		echo "Invalid threads number, should be a positive integer." >&2
		exit 1
	fi

	if [[ "$#" == 2 ]]
	then
		FORCE_PARALLEL=""
	else
		if [[ "$3" == "force_parallel" ]]
		then
			FORCE_PARALLEL="-p"
		else
			echo "Invalid third parameter. Should be 'force_parallel' or be omitted." >&2
	                exit 1
		fi
	fi
fi

VARIABLES=`cat $CNF | grep "p cnf" | cut -d " " -f 3`
CLAUSES=`cat $CNF | grep "p cnf" | cut -d " " -f 4`

#echo $VARIABLES $CLAUSES

for i in $(seq 1 $VARIABLES)
do

	let INDEX=$i-1

	CUDAPSAT_RESULT[$INDEX]="u"

done

$CUDAPSAT $CNF -t $THREADS $FORCE_PARALLEL -u OFF > $TMP_FILE

SAT=`cat $TMP_FILE | egrep "SAT|UNSAT|UNDEF"`
SOLUTIONS=`cat $TMP_FILE | egrep -x "((-)?[1-9][0-9]* )+0"`

if [[ $SAT != "UNDEF" ]] && [[ $SAT != "UNSAT" ]] && [[ $SAT != "SAT" ]]
then

	echo "GPU SAT Solver returned an unknown output." >&2
	echo "Instead of the SAT status it returned: $SAT"
	exit 2

fi

if [[ $SAT == "UNDEF" ]]
then
	echo "CUDA SAT Solver did not return answer..." >&2
	exit 2
fi

CPU_UNSAT=`grep -c "UNSAT" $SOLUTIONS_FILE`

if [[ "$CPU_UNSAT" != "1" ]] && [[ "$CPU_UNSAT" != "0" ]]
then

	echo "CPU SAT Solver printed unexpected results." >&2
	exit 2

fi

if [[ $SAT == "UNSAT" ]]
then

	if [[ "$CPU_UNSAT" == "1" ]]
	then
		echo "MATCHED"
		echo "Both are UNSAT"
		exit 10
	else
		echo "NOT MATCHED"
		echo "GPU returns UNSAT while CPU returns SAT"
		exit 20
	fi

else
	if [[ "$CPU_UNSAT" == "1" ]]
        then
		echo "NOT MATCHED"
                echo "GPU returns SAT while CPU returns UNSAT"
                exit 20
        fi
fi

for lit in $SOLUTIONS
do

	if [[ "$lit" != "0" ]]
	then
		VAR=`echo $lit | sed s/"-"//g`
                AUX=`echo $lit | grep -c "-"`

                 if [[ $AUX == "1" ]]
                 then
                         SIGN=f
                 else
                         SIGN=t
                 fi

		let INDEX=${VAR}-1
		CUDAPSAT_RESULT[$INDEX]=$SIGN
	fi

done

#echo $SOLUTIONS

MOST_CORRECT_VARIABLES=0

while read line
do

	CORRECT_VARIABLES=0

#	if [[ "$lit" == "$SOLUTIONS" ]]
#	then
#		echo "The same!"
#	fi

	for lit in $line
	do

		if [[ "$lit" != "0" ]]
		then
			VAR=`echo $lit | sed s/"-"//g`
			AUX=`echo $lit | grep -c "-"`

			if [[ $AUX == "1" ]]
			then
				SIGN=f
			else
				SIGN=t
			fi

			let INDEX=${VAR}-1
			CUDA_RES=${CUDAPSAT_RESULT[$INDEX]}

			if [[ "$CUDA_RES" == $SIGN ]] || [[ "$CUDA_RES" == "u" ]]
			then
				let CORRECT_VARIABLES++
			fi

		fi

	done

	if [ "$CORRECT_VARIABLES" -gt "$MOST_CORRECT_VARIABLES" ]
	then
		MOST_CORRECT_VARIABLES=$CORRECT_VARIABLES
	fi

	if [[ "$CORRECT_VARIABLES" == "$VARIABLES" ]]
	then
		echo "MATCHED"
		echo "Both are SAT and match with solution: $line"
		exit 10
	fi

done < $SOLUTIONS_FILE

rm $TMP_FILE

echo "NOT MATCHED"
echo "Only $MOST_CORRECT_VARIABLES variables matched from $VARIABLES"
exit 20
